(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, EXP).
The TRS R consists of the following rules:
:(:(x, y), z) → :(x, :(y, z))
:(+(x, y), z) → +(:(x, z), :(y, z))
:(z, +(x, f(y))) → :(g(z, y), +(x, a))
Rewrite Strategy: INNERMOST
(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)
The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
:(:(x, y), z) → :(x, :(y, z))
(2) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, EXP).
The TRS R consists of the following rules:
:(+(x, y), z) → +(:(x, z), :(y, z))
:(z, +(x, f(y))) → :(g(z, y), +(x, a))
Rewrite Strategy: INNERMOST
(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to weighted TRS
(4) Obligation:
The Runtime Complexity (innermost) of the given
CpxWeightedTrs could be proven to be
BOUNDS(1, EXP).
The TRS R consists of the following rules:
:(+(x, y), z) → +(:(x, z), :(y, z)) [1]
:(z, +(x, f(y))) → :(g(z, y), +(x, a)) [1]
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:
:(+(x, y), z) → +(:(x, z), :(y, z)) [1]
:(z, +(x, f(y))) → :(g(z, y), +(x, a)) [1]
The TRS has the following type information:
: :: +:f:g:a → +:f:g:a → +:f:g:a
+ :: +:f:g:a → +:f:g:a → +:f:g:a
f :: a → +:f:g:a
g :: +:f:g:a → a → +:f:g:a
a :: +:f:g:a
|
Rewrite Strategy: INNERMOST
(7) CompletionProof (UPPER BOUND(ID) transformation)
The transformation into a RNTS is sound, since:
(a) The obligation is a constructor system where every type has a constant constructor,
(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:
:
(c) The following functions are completely defined:
none
Due to the following rules being added:
none
And the following fresh constants:
const
(8) Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:
:(+(x, y), z) → +(:(x, z), :(y, z)) [1]
:(z, +(x, f(y))) → :(g(z, y), +(x, a)) [1]
The TRS has the following type information:
: :: +:f:g:a → +:f:g:a → +:f:g:a
+ :: +:f:g:a → +:f:g:a → +:f:g:a
f :: a → +:f:g:a
g :: +:f:g:a → a → +:f:g:a
a :: +:f:g:a
const :: a
|
Rewrite Strategy: INNERMOST |
(9) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
(10) Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:
:(+(x, y), z) → +(:(x, z), :(y, z)) [1]
:(z, +(x, f(y))) → :(g(z, y), +(x, a)) [1]
The TRS has the following type information:
: :: +:f:g:a → +:f:g:a → +:f:g:a
+ :: +:f:g:a → +:f:g:a → +:f:g:a
f :: a → +:f:g:a
g :: +:f:g:a → a → +:f:g:a
a :: +:f:g:a
const :: a
|
Rewrite Strategy: INNERMOST |
(11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:
a => 0
const => 0
(12) Obligation:
Complexity RNTS consisting of the following rules:
:(z', z'') -{ 1 }→ :(1 + z + y, 1 + x + 0) :|: z >= 0, x >= 0, y >= 0, z'' = 1 + x + (1 + y), z' = z
:(z', z'') -{ 1 }→ 1 + :(x, z) + :(y, z) :|: z'' = z, z >= 0, z' = 1 + x + y, x >= 0, y >= 0
(13) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
(14) Obligation:
Complexity RNTS consisting of the following rules:
:(z', z'') -{ 1 }→ :(1 + z' + y, 1 + x + 0) :|: z' >= 0, x >= 0, y >= 0, z'' = 1 + x + (1 + y)
:(z', z'') -{ 1 }→ 1 + :(x, z'') + :(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
(15) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)
Found the following analysis order by SCC decomposition:
(16) Obligation:
Complexity RNTS consisting of the following rules:
:(z', z'') -{ 1 }→ :(1 + z' + y, 1 + x + 0) :|: z' >= 0, x >= 0, y >= 0, z'' = 1 + x + (1 + y)
:(z', z'') -{ 1 }→ 1 + :(x, z'') + :(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
Function symbols to be analyzed: {
:}
(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)
Computed SIZE bound using CoFloCo for: :
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0
(18) Obligation:
Complexity RNTS consisting of the following rules:
:(z', z'') -{ 1 }→ :(1 + z' + y, 1 + x + 0) :|: z' >= 0, x >= 0, y >= 0, z'' = 1 + x + (1 + y)
:(z', z'') -{ 1 }→ 1 + :(x, z'') + :(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
Function symbols to be analyzed: {
:}
Previous analysis results are:
:: runtime: ?, size: O(1) [0]
|
(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)
Computed RUNTIME bound using PUBS for: :
after applying outer abstraction to obtain an ITS,
resulting in: EXP with polynomial bound: ?
(20) Obligation:
Complexity RNTS consisting of the following rules:
:(z', z'') -{ 1 }→ :(1 + z' + y, 1 + x + 0) :|: z' >= 0, x >= 0, y >= 0, z'' = 1 + x + (1 + y)
:(z', z'') -{ 1 }→ 1 + :(x, z'') + :(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
Function symbols to be analyzed:
Previous analysis results are:
:: runtime: EXP, size: O(1) [0]
|
(21) FinalProof (EQUIVALENT transformation)
Computed overall runtime complexity
(22) BOUNDS(1, EXP)